<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>UseTactics: Tactic Library for Coq: A Gentle Introduction</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">UseTactics: Tactic Library for Coq<span class="subtitle">A Gentle Introduction</span></h1>

<div class="code">
</div>

<div class="code">

<br/>
<span class="comment">(*&nbsp;Chapter&nbsp;written&nbsp;and&nbsp;maintained&nbsp;by&nbsp;Arthur&nbsp;Chargueraud&nbsp;*)</span><br/>
</div>

<div class="doc">
Coq comes with a set of builtin tactics, such as <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span>,
    <span class="inlinecode"><span class="id" title="tactic">intros</span></span>, <span class="inlinecode"><span class="id" title="tactic">inversion</span></span> and so on. While it is possible to conduct
    proofs using only those tactics, you can significantly increase
    your productivity by working with a set of more powerful tactics.
    This chapter describes a number of such useful tactics, which, for
    various reasons, are not yet available by default in Coq.  These
    tactics are defined in the <span class="inlinecode"><span class="id" title="var">LibTactics.v</span></span> file. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-notation-overridden,-parsing".<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.Arith.html#"><span class="id" title="library">Arith.Arith</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="library">Maps</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="Stlc.html#"><span class="id" title="library">Stlc</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="Types.html#"><span class="id" title="library">Types</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="Smallstep.html#"><span class="id" title="library">Smallstep</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="LibTactics.html#"><span class="id" title="library">LibTactics</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="Equiv.html#"><span class="id" title="library">Equiv</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="References.html#"><span class="id" title="library">References</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="Hoare.html#"><span class="id" title="library">Hoare</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="Sub.html#"><span class="id" title="library">Sub</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">LibTactics</span>.<br/>
</div>

<div class="doc">
Remark: SSReflect is another package providing powerful tactics.
    The library "LibTactics" differs from "SSReflect" in two respects:
<ul class="doclist">
<li> "SSReflect" was primarily developed for proving mathematical
          theorems, whereas "LibTactics" was primarily developed for proving
          theorems on programming languages. In particular, "LibTactics"
          provides a number of useful tactics that have no counterpart in the
          "SSReflect" package.

</li>
<li> "SSReflect" entirely rethinks the presentation of tactics,
          whereas "LibTactics" mostly stick to the traditional
          presentation of Coq tactics, simply providing a number of
          additional tactics.  For this reason, "LibTactics" is
          probably easier to get started with than "SSReflect". 
</li>
</ul>

<div class="paragraph"> </div>

 This chapter is a tutorial focusing on the most useful features
    from the "LibTactics" library. It does not aim at presenting all
    the features of "LibTactics". The detailed specification of tactics
    can be found in the source file <span class="inlinecode"><span class="id" title="var">LibTactics.v</span></span>. Further documentation
    as well as demos can be found at <a href="https://www.chargueraud.org/softs/tlc/"><span class="inlineref">https://www.chargueraud.org/softs/tlc/</span></a>. 
<div class="paragraph"> </div>

 In this tutorial, tactics are presented using examples taken from
    the core chapters of the "Software Foundations" course. To illustrate
    the various ways in which a given tactic can be used, we use a
    tactic that duplicates a given goal. More precisely, <span class="inlinecode"><span class="id" title="var">dup</span></span> produces
    two copies of the current goal, and <span class="inlinecode"><span class="id" title="var">dup</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> produces <span class="inlinecode"><span class="id" title="var">n</span></span> copies of it. 
</div>

<div class="doc">
<a id="lab543"></a><h1 class="section">Tactics for Naming and Performing Inversion</h1>

<div class="paragraph"> </div>

 This section presents the following tactics:
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">introv</span></span>, for naming hypotheses more efficiently,

</li>
<li> <span class="inlinecode"><span class="id" title="var">inverts</span></span>, for improving the <span class="inlinecode"><span class="id" title="tactic">inversion</span></span> tactic. 
</li>
</ul>

</div>

<div class="doc">
<a id="lab544"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">introv</span></span></h2>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="IntrovExamples" class="idref" href="#IntrovExamples"><span class="id" title="module">IntrovExamples</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Maps</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Imp</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Equiv</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Stlc</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">introv</span></span> allows to automatically introduce the
    variables of a theorem and explicitly name the hypotheses
    involved. In the example shown next, the variables <span class="inlinecode"><span class="id" title="var">c</span></span>,
    <span class="inlinecode"><span class="id" title="var">st</span></span>, <span class="inlinecode"><span class="id" title="var">st<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" title="var">st<sub>2</sub></span></span> involved in the statement of determinism
    need not be named explicitly, because their name where already
    given in the statement of the lemma. On the contrary, it is
    useful to provide names for the two hypotheses, which we
    name <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span>, respectively. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="IntrovExamples.ceval_deterministic" class="idref" href="#IntrovExamples.ceval_deterministic"><span class="id" title="lemma">ceval_deterministic</span></a>: <span class="id" title="keyword">∀</span> <a id="c:1" class="idref" href="#c:1"><span class="id" title="binder">c</span></a> <a id="st:2" class="idref" href="#st:2"><span class="id" title="binder">st</span></a> <a id="st<sub>1</sub>:3" class="idref" href="#st<sub>1</sub>:3"><span class="id" title="binder">st<sub>1</sub></span></a> <a id="st<sub>2</sub>:4" class="idref" href="#st<sub>2</sub>:4"><span class="id" title="binder">st<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:2"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:1"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>1</sub>:3"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:2"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:1"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>2</sub>:4"><span class="id" title="variable">st<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st<sub>1</sub>:3"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#st<sub>2</sub>:4"><span class="id" title="variable">st<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> <span class="id" title="var">E<sub>1</sub></span> <span class="id" title="var">E<sub>2</sub></span>. <span class="comment">(*&nbsp;was&nbsp;<span class="inlinecode"><span class="id" title="tactic">intros</span></span> <span class="inlinecode"><span class="id" title="var">c</span></span> <span class="inlinecode"><span class="id" title="var">st</span></span> <span class="inlinecode"><span class="id" title="var">st<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">st<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span>&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
When there is no hypothesis to be named, one can call
    <span class="inlinecode"><span class="id" title="var">introv</span></span> without any argument. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="IntrovExamples.dist_exists_or" class="idref" href="#IntrovExamples.dist_exists_or"><span class="id" title="lemma">dist_exists_or</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:5" class="idref" href="#X:5"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>) (<a id="P:6" class="idref" href="#P:6"><span class="id" title="binder">P</span></a> <a id="Q:7" class="idref" href="#Q:7"><span class="id" title="binder">Q</span></a> : <a class="idref" href="UseTactics.html#X:5"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'&lt;-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="x:8" class="idref" href="#x:8"><span class="id" title="binder">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="UseTactics.html#P:6"><span class="id" title="variable">P</span></a> <a class="idref" href="UseTactics.html#x:8"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="UseTactics.html#Q:7"><span class="id" title="variable">Q</span></a> <a class="idref" href="UseTactics.html#x:8"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'&lt;-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'&lt;-&gt;'_x"><span class="id" title="notation">↔</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="x:9" class="idref" href="#x:9"><span class="id" title="binder">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="UseTactics.html#P:6"><span class="id" title="variable">P</span></a> <a class="idref" href="UseTactics.html#x:9"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="x:10" class="idref" href="#x:10"><span class="id" title="binder">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="UseTactics.html#Q:7"><span class="id" title="variable">Q</span></a> <a class="idref" href="UseTactics.html#x:10"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span>. <span class="comment">(*&nbsp;was&nbsp;<span class="inlinecode"><span class="id" title="tactic">intros</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">Q</span></span>&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">introv</span></span> also applies to statements in which
    <span class="inlinecode"><span class="id" title="keyword">∀</span></span> and <span class="inlinecode">→</span> are interleaved. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="IntrovExamples.ceval_deterministic'" class="idref" href="#IntrovExamples.ceval_deterministic'"><span class="id" title="lemma">ceval_deterministic'</span></a>: <span class="id" title="keyword">∀</span> <a id="c:11" class="idref" href="#c:11"><span class="id" title="binder">c</span></a> <a id="st:12" class="idref" href="#st:12"><span class="id" title="binder">st</span></a> <a id="st<sub>1</sub>:13" class="idref" href="#st<sub>1</sub>:13"><span class="id" title="binder">st<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="UseTactics.html#st:12"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:11"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>1</sub>:13"><span class="id" title="variable">st<sub>1</sub></span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <a id="st<sub>2</sub>:14" class="idref" href="#st<sub>2</sub>:14"><span class="id" title="binder">st<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="UseTactics.html#st:12"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:11"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>2</sub>:14"><span class="id" title="variable">st<sub>2</sub></span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st<sub>1</sub>:13"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#st<sub>2</sub>:14"><span class="id" title="variable">st<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> <span class="id" title="var">E<sub>1</sub></span> <span class="id" title="var">E<sub>2</sub></span>. <span class="comment">(*&nbsp;was&nbsp;<span class="inlinecode"><span class="id" title="tactic">intros</span></span> <span class="inlinecode"><span class="id" title="var">c</span></span> <span class="inlinecode"><span class="id" title="var">st</span></span> <span class="inlinecode"><span class="id" title="var">st<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">st<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span>&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
Like the arguments of <span class="inlinecode"><span class="id" title="tactic">intros</span></span>, the arguments of <span class="inlinecode"><span class="id" title="var">introv</span></span>
    can be structured patterns. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="IntrovExamples.exists_impl" class="idref" href="#IntrovExamples.exists_impl"><span class="id" title="lemma">exists_impl</span></a>: <span class="id" title="keyword">∀</span> <a id="X:15" class="idref" href="#X:15"><span class="id" title="binder">X</span></a> (<a id="P:16" class="idref" href="#P:16"><span class="id" title="binder">P</span></a> : <a class="idref" href="UseTactics.html#X:15"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<a id="Q:17" class="idref" href="#Q:17"><span class="id" title="binder">Q</span></a> : <span class="id" title="keyword">Prop</span>) (<a id="R:18" class="idref" href="#R:18"><span class="id" title="binder">R</span></a> : <span class="id" title="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <a id="x:20" class="idref" href="#x:20"><span class="id" title="binder">x</span></a>, <a class="idref" href="UseTactics.html#P:16"><span class="id" title="variable">P</span></a> <a class="idref" href="UseTactics.html#x:20"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="UseTactics.html#Q:17"><span class="id" title="variable">Q</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">((</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="x:19" class="idref" href="#x:19"><span class="id" title="binder">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="UseTactics.html#P:16"><span class="id" title="variable">P</span></a> <a class="idref" href="UseTactics.html#x:19"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="UseTactics.html#Q:17"><span class="id" title="variable">Q</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> [<span class="id" title="var">x</span> <span class="id" title="var">H<sub>2</sub></span>]. <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;same&nbsp;as&nbsp;<span class="inlinecode"><span class="id" title="tactic">intros</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">Q</span></span> <span class="inlinecode"><span class="id" title="var">R</span></span> <span class="inlinecode"><span class="id" title="var">H<sub>1</sub></span></span> <span class="inlinecode">[<span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span>].</span>,&nbsp;which&nbsp;is&nbsp;itself&nbsp;short<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;for&nbsp;<span class="inlinecode"><span class="id" title="tactic">intros</span></span> <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">Q</span></span> <span class="inlinecode"><span class="id" title="var">R</span></span> <span class="inlinecode"><span class="id" title="var">H<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span>.</span> <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="keyword">as</span></span> <span class="inlinecode">[<span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span>].</span>&nbsp;*)</span><br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Remark: the tactic <span class="inlinecode"><span class="id" title="var">introv</span></span> works even when definitions
    need to be unfolded in order to reveal hypotheses. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#IntrovExamples"><span class="id" title="module">IntrovExamples</span></a>.<br/>
</div>

<div class="doc">
<a id="lab545"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">inverts</span></span></h2>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="InvertsExamples" class="idref" href="#InvertsExamples"><span class="id" title="module">InvertsExamples</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Maps</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Imp</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Equiv</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" title="tactic">inversion</span></span> tactic of Coq is not very satisfying for
    three reasons. First, it produces a bunch of equalities
    which one typically wants to substitute away, using <span class="inlinecode"><span class="id" title="tactic">subst</span></span>.
    Second, it introduces meaningless names for hypotheses.
    Third, a call to <span class="inlinecode"><span class="id" title="tactic">inversion</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> does not remove <span class="inlinecode"><span class="id" title="var">H</span></span> from the
    context, even though in most cases an hypothesis is no longer
    needed after being inverted. The tactic <span class="inlinecode"><span class="id" title="var">inverts</span></span> address all
    of these three issues. It is intented to be used in place of
    the tactic <span class="inlinecode"><span class="id" title="tactic">inversion</span></span>. 
<div class="paragraph"> </div>

 The following example illustrates how the tactic <span class="inlinecode"><span class="id" title="var">inverts</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>
    behaves mostly like <span class="inlinecode"><span class="id" title="tactic">inversion</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> except that it performs
    some substitutions in order to eliminate the trivial equalities
    that are being produced by <span class="inlinecode"><span class="id" title="tactic">inversion</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="InvertsExamples.skip_left" class="idref" href="#InvertsExamples.skip_left"><span class="id" title="lemma">skip_left</span></a>: <span class="id" title="keyword">∀</span> <a id="c:21" class="idref" href="#c:21"><span class="id" title="binder">c</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Equiv.html#cequiv"><span class="id" title="definition">cequiv</span></a> <span class="id" title="notation">&lt;{</span><span class="id" title="notation">skip</span><span class="id" title="notation">;</span> <a class="idref" href="UseTactics.html#c:21"><span class="id" title="variable">c</span></a><span class="id" title="notation">}&gt;</span> <a class="idref" href="UseTactics.html#c:21"><span class="id" title="variable">c</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span>. <span class="id" title="tactic">split</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">dup</span>. <span class="comment">(*&nbsp;duplicate&nbsp;the&nbsp;goal&nbsp;for&nbsp;comparison&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;was...&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">subst</span>. <span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>2</sub></span>. <span class="id" title="tactic">subst</span>. <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;now...&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" title="var">inverts</span> <span class="id" title="var">H</span>. <span class="id" title="var">inverts</span> <span class="id" title="var">H<sub>2</sub></span>. <span class="id" title="tactic">assumption</span>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
A slightly more interesting example appears next. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="InvertsExamples.ceval_deterministic" class="idref" href="#InvertsExamples.ceval_deterministic"><span class="id" title="lemma">ceval_deterministic</span></a>: <span class="id" title="keyword">∀</span> <a id="c:22" class="idref" href="#c:22"><span class="id" title="binder">c</span></a> <a id="st:23" class="idref" href="#st:23"><span class="id" title="binder">st</span></a> <a id="st<sub>1</sub>:24" class="idref" href="#st<sub>1</sub>:24"><span class="id" title="binder">st<sub>1</sub></span></a> <a id="st<sub>2</sub>:25" class="idref" href="#st<sub>2</sub>:25"><span class="id" title="binder">st<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:23"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:22"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>1</sub>:24"><span class="id" title="variable">st<sub>1</sub></span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:23"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:22"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>2</sub>:25"><span class="id" title="variable">st<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st<sub>1</sub>:24"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#st<sub>2</sub>:25"><span class="id" title="variable">st<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> <span class="id" title="var">E<sub>1</sub></span> <span class="id" title="var">E<sub>2</sub></span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">E<sub>1</sub></span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">st<sub>2</sub></span> <span class="id" title="var">E<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">admit</span>. <span class="id" title="var">admit</span>. <span class="comment">(*&nbsp;skip&nbsp;some&nbsp;basic&nbsp;cases&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">dup</span>. <span class="comment">(*&nbsp;duplicate&nbsp;the&nbsp;goal&nbsp;for&nbsp;comparison&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;was:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" title="tactic">inversion</span> <span class="id" title="var">E<sub>2</sub></span>. <span class="id" title="tactic">subst</span>. <span class="id" title="var">admit</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;now:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" title="var">inverts</span> <span class="id" title="var">E<sub>2</sub></span>. <span class="id" title="var">admit</span>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">inverts</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="keyword">as</span>.</span> is like <span class="inlinecode"><span class="id" title="var">inverts</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> except that the
    variables and hypotheses being produced are placed in the goal
    rather than in the context. This strategy allows naming those
    new variables and hypotheses explicitly, using either <span class="inlinecode"><span class="id" title="tactic">intros</span></span>
    or <span class="inlinecode"><span class="id" title="var">introv</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="InvertsExamples.ceval_deterministic'" class="idref" href="#InvertsExamples.ceval_deterministic'"><span class="id" title="lemma">ceval_deterministic'</span></a>: <span class="id" title="keyword">∀</span> <a id="c:26" class="idref" href="#c:26"><span class="id" title="binder">c</span></a> <a id="st:27" class="idref" href="#st:27"><span class="id" title="binder">st</span></a> <a id="st<sub>1</sub>:28" class="idref" href="#st<sub>1</sub>:28"><span class="id" title="binder">st<sub>1</sub></span></a> <a id="st<sub>2</sub>:29" class="idref" href="#st<sub>2</sub>:29"><span class="id" title="binder">st<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:27"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:26"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>1</sub>:28"><span class="id" title="variable">st<sub>1</sub></span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:27"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:26"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>2</sub>:29"><span class="id" title="variable">st<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st<sub>1</sub>:28"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#st<sub>2</sub>:29"><span class="id" title="variable">st<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> <span class="id" title="var">E<sub>1</sub></span> <span class="id" title="var">E<sub>2</sub></span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">E<sub>1</sub></span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">st<sub>2</sub></span> <span class="id" title="var">E<sub>2</sub></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">E<sub>2</sub></span> <span class="id" title="keyword">as</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Skip&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Ass&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Observe&nbsp;that&nbsp;the&nbsp;variable&nbsp;<span class="inlinecode"><span class="id" title="var">n</span></span>&nbsp;is&nbsp;not&nbsp;automatically<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;substituted&nbsp;because,&nbsp;contrary&nbsp;to&nbsp;<span class="inlinecode"><span class="id" title="tactic">inversion</span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span>;</span> <span class="inlinecode"><span class="id" title="tactic">subst</span></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;the&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" title="var">inverts</span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span>&nbsp;does&nbsp;not&nbsp;substitute&nbsp;the&nbsp;equalities<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;that&nbsp;exist&nbsp;before&nbsp;running&nbsp;the&nbsp;inversion.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;*)</span> <span class="id" title="tactic">subst</span> <span class="id" title="var">n</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Seq&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Here,&nbsp;the&nbsp;newly&nbsp;created&nbsp;variables&nbsp;can&nbsp;be&nbsp;introduced<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;using&nbsp;intros,&nbsp;so&nbsp;they&nbsp;can&nbsp;be&nbsp;assigned&nbsp;meaningful&nbsp;names,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;for&nbsp;example&nbsp;<span class="inlinecode"><span class="id" title="var">st<sub>3</sub></span></span>&nbsp;instead&nbsp;of&nbsp;<span class="inlinecode"><span class="id" title="var">st'0</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;*)</span> <span class="id" title="tactic">intros</span> <span class="id" title="var">st<sub>3</sub></span> <span class="id" title="var">Red1</span> <span class="id" title="var">Red2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<span class="id" title="var">st'</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">st<sub>3</sub></span>) <span class="id" title="keyword">as</span> <span class="id" title="var">EQ<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;Proof&nbsp;of&nbsp;assertion&nbsp;*)</span> <span class="id" title="tactic">apply</span> <span class="id" title="var">IHE1_1</span>; <span class="id" title="tactic">assumption</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">subst</span> <span class="id" title="var">st<sub>3</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHE1_2</span>. <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;E_IfTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;In&nbsp;an&nbsp;easy&nbsp;case&nbsp;like&nbsp;this&nbsp;one,&nbsp;there&nbsp;is&nbsp;no&nbsp;need&nbsp;to<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;provide&nbsp;meaningful&nbsp;names,&nbsp;so&nbsp;we&nbsp;can&nbsp;just&nbsp;use&nbsp;<span class="inlinecode"><span class="id" title="tactic">intros</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;*)</span> <span class="id" title="tactic">intros</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHE1</span>. <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;false&nbsp;(contradiction)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;*)</span> <span class="id" title="tactic">intros</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H<sub>5</sub></span>. <span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;other&nbsp;cases&nbsp;are&nbsp;similiar&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
In the particular case where a call to <span class="inlinecode"><span class="id" title="tactic">inversion</span></span> produces
    a single subgoal, one can use the syntax <span class="inlinecode"><span class="id" title="var">inverts</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="keyword">as</span></span> <span class="inlinecode"><span class="id" title="var">H<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">H<sub>3</sub></span></span>
    for calling <span class="inlinecode"><span class="id" title="var">inverts</span></span> and naming the new hypotheses <span class="inlinecode"><span class="id" title="var">H<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span></span>
    and <span class="inlinecode"><span class="id" title="var">H<sub>3</sub></span></span>. In other words, the tactic <span class="inlinecode"><span class="id" title="var">inverts</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="keyword">as</span></span> <span class="inlinecode"><span class="id" title="var">H<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">H<sub>3</sub></span></span> is
    equivalent to <span class="inlinecode"><span class="id" title="var">inverts</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="keyword">as</span>;</span> <span class="inlinecode"><span class="id" title="var">introv</span></span> <span class="inlinecode"><span class="id" title="var">H<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">H<sub>3</sub></span></span>. An example follows. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="InvertsExamples.skip_left'" class="idref" href="#InvertsExamples.skip_left'"><span class="id" title="lemma">skip_left'</span></a>: <span class="id" title="keyword">∀</span> <a id="c:30" class="idref" href="#c:30"><span class="id" title="binder">c</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Equiv.html#cequiv"><span class="id" title="definition">cequiv</span></a> <span class="id" title="notation">&lt;{</span> <span class="id" title="notation">skip</span> <span class="id" title="notation">;</span> <a class="idref" href="UseTactics.html#c:30"><span class="id" title="variable">c</span></a><span class="id" title="notation">}&gt;</span> <a class="idref" href="UseTactics.html#c:30"><span class="id" title="variable">c</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span>. <span class="id" title="tactic">split</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> <span class="id" title="var">U</span> <span class="id" title="var">V</span>. <span class="comment">(*&nbsp;new&nbsp;hypotheses&nbsp;are&nbsp;named&nbsp;<span class="inlinecode"><span class="id" title="var">U</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">V</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">U</span>. <span class="id" title="tactic">assumption</span>.<br/>
<span class="id" title="keyword">Abort</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#InvertsExamples"><span class="id" title="module">InvertsExamples</span></a>.<br/>
</div>

<div class="doc">
A more involved example appears next. In particular, this example
    shows that the name of the hypothesis being inverted can be reused. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="InvertsExamples1" class="idref" href="#InvertsExamples1"><span class="id" title="module">InvertsExamples1</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="keyword">Types</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Stlc</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">STLC</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Maps</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="InvertsExamples1.typing_nonexample_1" class="idref" href="#InvertsExamples1.typing_nonexample_1"><span class="id" title="definition">typing_nonexample_1</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="T:31" class="idref" href="#T:31"><span class="id" title="binder">T</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">(</span></a><a class="idref" href="Stlc.html#STLC.x"><span class="id" title="definition">x</span></a> <a class="idref" href="Stlc.html#STLC.y"><span class="id" title="definition">y</span></a><a class="idref" href="Stlc.html#356f9b00d0ca8b465f5c07428196b78a"><span class="id" title="notation">)</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="UseTactics.html#T:31"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">dup</span> 3.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;old&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;-  <span class="id" title="tactic">intros</span> <span class="id" title="var">Hc</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">Hc</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T</span> <span class="id" title="var">Hc</span>].<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">Hc</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">Hc</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>4</sub></span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>5</sub></span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H<sub>5</sub></span> <span class="id" title="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>2</sub></span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">discriminate</span> <span class="id" title="var">H<sub>1</sub></span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" title="tactic">intros</span> <span class="id" title="var">C</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">C</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H<sub>2</sub></span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>3</sub></span> <span class="id" title="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H<sub>3</sub></span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H<sub>5</sub></span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof,&nbsp;alternative:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" title="tactic">intros</span> <span class="id" title="var">C</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">C</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">inverts</span> <span class="id" title="var">H<sub>1</sub></span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#InvertsExamples1"><span class="id" title="module">InvertsExamples1</span></a>.<br/>
</div>

<div class="doc">
Note: in the rare cases where one needs to perform an inversion
    on an hypothesis <span class="inlinecode"><span class="id" title="var">H</span></span> without clearing <span class="inlinecode"><span class="id" title="var">H</span></span> from the context,
    one can use the tactic <span class="inlinecode"><span class="id" title="var">inverts</span></span> <span class="inlinecode"><span class="id" title="var">keep</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>, where the keyword <span class="inlinecode"><span class="id" title="var">keep</span></span>
    indicates that the hypothesis should be kept in the context. 
</div>

<div class="doc">
<a id="lab546"></a><h1 class="section">Tactics for N-ary Connectives</h1>

<div class="paragraph"> </div>

 Because Coq encodes conjunctions and disjunctions using binary
    constructors <span class="inlinecode">∧</span> and <span class="inlinecode">∨</span>, working with a conjunction or a
    disjunction of <span class="inlinecode"><span class="id" title="var">N</span></span> facts can sometimes be quite cumbursome.
    For this reason, "LibTactics" provides tactics offering direct
    support for n-ary conjunctions and disjunctions. It also provides
    direct support for n-ary existententials. 
<div class="paragraph"> </div>

 This section presents the following tactics:
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">splits</span></span> for decomposing n-ary conjunctions,

</li>
<li> <span class="inlinecode"><span class="id" title="var">branch</span></span> for decomposing n-ary disjunctions 
</li>
</ul>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="NaryExamples" class="idref" href="#NaryExamples"><span class="id" title="module">NaryExamples</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">References</span>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">Smallstep</span>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">STLCRef</span>.<br/>
</div>

<div class="doc">
<a id="lab547"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">splits</span></span></h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">splits</span></span> applies to a goal made of a conjunction
    of <span class="inlinecode"><span class="id" title="var">n</span></span> propositions and it produces <span class="inlinecode"><span class="id" title="var">n</span></span> subgoals. For example,
    it decomposes the goal <span class="inlinecode"><span class="id" title="var">G<sub>1</sub></span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" title="var">G<sub>2</sub></span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" title="var">G<sub>3</sub></span></span> into the three subgoals
    <span class="inlinecode"><span class="id" title="var">G<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" title="var">G<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" title="var">G<sub>3</sub></span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="NaryExamples.demo_splits" class="idref" href="#NaryExamples.demo_splits"><span class="id" title="lemma">demo_splits</span></a> : <span class="id" title="keyword">∀</span> <a id="n:32" class="idref" href="#n:32"><span class="id" title="binder">n</span></a> <a id="m:33" class="idref" href="#m:33"><span class="id" title="binder">m</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#n:32"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&gt;'_x"><span class="id" title="notation">&gt;</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="UseTactics.html#n:32"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&lt;'_x"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="UseTactics.html#m:33"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="UseTactics.html#m:33"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&lt;'_x"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="UseTactics.html#n:32"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a>10 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="UseTactics.html#m:33"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'&lt;&gt;'_x"><span class="id" title="notation">≠</span></a> 3.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span>. <span class="id" title="var">splits</span>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
<a id="lab548"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">branch</span></span></h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">branch</span></span> <span class="inlinecode"><span class="id" title="var">k</span></span> can be used to prove a n-ary disjunction.
    For example, if the goal takes the form <span class="inlinecode"><span class="id" title="var">G<sub>1</sub></span></span> <span class="inlinecode">∨</span> <span class="inlinecode"><span class="id" title="var">G<sub>2</sub></span></span> <span class="inlinecode">∨</span> <span class="inlinecode"><span class="id" title="var">G<sub>3</sub></span></span>,
    the tactic <span class="inlinecode"><span class="id" title="var">branch</span></span> <span class="inlinecode">2</span> leaves only <span class="inlinecode"><span class="id" title="var">G<sub>2</sub></span></span> as subgoal. The following
    example illustrates the behavior of the <span class="inlinecode"><span class="id" title="var">branch</span></span> tactic. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="NaryExamples.demo_branch" class="idref" href="#NaryExamples.demo_branch"><span class="id" title="lemma">demo_branch</span></a> : <span class="id" title="keyword">∀</span> <a id="n:34" class="idref" href="#n:34"><span class="id" title="binder">n</span></a> <a id="m:35" class="idref" href="#m:35"><span class="id" title="binder">m</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#n:34"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&lt;'_x"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="UseTactics.html#m:35"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="UseTactics.html#n:34"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#m:35"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="UseTactics.html#m:35"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&lt;'_x"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="UseTactics.html#n:34"><span class="id" title="variable">n</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<a class="idref" href="http://coq.inria.fr/library//Coq.Arith.Compare_dec.html#lt_eq_lt_dec"><span class="id" title="definition">lt_eq_lt_dec</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) <span class="id" title="keyword">as</span> [ [<span class="id" title="var">H<sub>1</sub></span>|<span class="id" title="var">H<sub>2</sub></span>]|<span class="id" title="var">H<sub>3</sub></span>].<br/>
&nbsp;&nbsp;- <span class="id" title="var">branch</span> 1. <span class="id" title="tactic">apply</span> <span class="id" title="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;- <span class="id" title="var">branch</span> 2. <span class="id" title="tactic">apply</span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;- <span class="id" title="var">branch</span> 3. <span class="id" title="tactic">apply</span> <span class="id" title="var">H<sub>3</sub></span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#NaryExamples"><span class="id" title="module">NaryExamples</span></a>.<br/>
</div>

<div class="doc">
<a id="lab549"></a><h1 class="section">Tactics for Working with Equality</h1>

<div class="paragraph"> </div>

 One of the major weakness of Coq compared with other interactive
    proof assistants is its relatively poor support for reasoning
    with equalities. The tactics described next aims at simplifying
    pieces of proof scripts manipulating equalities. 
<div class="paragraph"> </div>

 This section presents the following tactics:
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span> for introducing an equality to rewrite with,

</li>
<li> <span class="inlinecode"><span class="id" title="var">cuts_rewrite</span></span>, which is similar except that its subgoals are swapped,

</li>
<li> <span class="inlinecode"><span class="id" title="var">substs</span></span> for improving the <span class="inlinecode"><span class="id" title="tactic">subst</span></span> tactic,

</li>
<li> <span class="inlinecode"><span class="id" title="var">fequals</span></span> for improving the <span class="inlinecode"><span class="id" title="tactic">f_equal</span></span> tactic,

</li>
<li> <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> for proving <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span> using an hypothesis <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">z</span></span>,
      automatically producing an equality <span class="inlinecode"><span class="id" title="var">y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">z</span></span> as subgoal. 
</li>
</ul>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="EqualityExamples" class="idref" href="#EqualityExamples"><span class="id" title="module">EqualityExamples</span></a>.<br/>
</div>

<div class="doc">
<a id="lab550"></a><h2 class="section">The Tactics <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span> and <span class="inlinecode"><span class="id" title="var">cuts_rewrite</span></span></h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span> <span class="inlinecode">(<span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span>)</span> replaces <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> with <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span> in
    the goal, and produces the goal <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="EqualityExamples.mult_0_plus" class="idref" href="#EqualityExamples.mult_0_plus"><span class="id" title="lemma">mult_0_plus</span></a> : <span class="id" title="keyword">∀</span> <a id="n:36" class="idref" href="#n:36"><span class="id" title="binder">n</span></a> <a id="m:37" class="idref" href="#m:37"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">(</span></a>0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="UseTactics.html#n:36"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#m:37"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#n:36"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#m:37"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">dup</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;old&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<span class="id" title="var">H</span>: 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">n</span>). <span class="id" title="tactic">reflexivity</span>. <span class="id" title="tactic">rewrite</span> → <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">asserts_rewrite</span> (0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">n</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>. <span class="comment">(*&nbsp;subgoal&nbsp;<span class="inlinecode">0+<span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">n</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>. <span class="comment">(*&nbsp;subgoal&nbsp;<span class="inlinecode"><span class="id" title="var">n</span>×<span class="id" title="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span>×<span class="id" title="var">n</span></span>&nbsp;*)</span><br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Remark: the syntax <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span> <span class="inlinecode">(<span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span>)</span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> allows
     rewriting in the hypothesis <span class="inlinecode"><span class="id" title="var">H</span></span> rather than in the goal. 
<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">cuts_rewrite</span></span> <span class="inlinecode">(<span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span>)</span> is like
    <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span> <span class="inlinecode">(<span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span>)</span>, except that the equality <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span>
    appears as first subgoal. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="EqualityExamples.mult_0_plus'" class="idref" href="#EqualityExamples.mult_0_plus'"><span class="id" title="lemma">mult_0_plus'</span></a> : <span class="id" title="keyword">∀</span> <a id="n:38" class="idref" href="#n:38"><span class="id" title="binder">n</span></a> <a id="m:39" class="idref" href="#m:39"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">(</span></a>0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="UseTactics.html#n:38"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#m:39"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#n:38"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#m:39"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">cuts_rewrite</span> (0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">n</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>. <span class="comment">(*&nbsp;subgoal&nbsp;<span class="inlinecode"><span class="id" title="var">n</span>×<span class="id" title="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span>×<span class="id" title="var">n</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>. <span class="comment">(*&nbsp;subgoal&nbsp;<span class="inlinecode">0+<span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">n</span></span>&nbsp;*)</span><br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
More generally, the tactics <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span> and <span class="inlinecode"><span class="id" title="var">cuts_rewrite</span></span>
    can be provided a lemma as argument. For example, one can write
    <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span> <span class="inlinecode">(<span class="id" title="keyword">∀</span></span> <span class="inlinecode"><span class="id" title="var">a</span></span> <span class="inlinecode"><span class="id" title="var">b</span>,</span> <span class="inlinecode"><span class="id" title="var">a</span>*(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">b</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">a</span>×<span class="id" title="var">b</span>+<span class="id" title="var">a</span>)</span>.
    This formulation is useful when <span class="inlinecode"><span class="id" title="var">a</span></span> and <span class="inlinecode"><span class="id" title="var">b</span></span> are big terms,
    since there is no need to repeat their statements. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="EqualityExamples.mult_0_plus''" class="idref" href="#EqualityExamples.mult_0_plus''"><span class="id" title="lemma">mult_0_plus''</span></a> : <span class="id" title="keyword">∀</span> <a id="u:40" class="idref" href="#u:40"><span class="id" title="binder">u</span></a> <a id="v:41" class="idref" href="#v:41"><span class="id" title="binder">v</span></a> <a id="w:42" class="idref" href="#w:42"><span class="id" title="binder">w</span></a> <a id="x:43" class="idref" href="#x:43"><span class="id" title="binder">x</span></a> <a id="y:44" class="idref" href="#y:44"><span class="id" title="binder">y</span></a> <a id="z:45" class="idref" href="#z:45"><span class="id" title="binder">z</span></a>: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="UseTactics.html#u:40"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="UseTactics.html#v:41"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="UseTactics.html#w:42"><span class="id" title="variable">w</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#x:43"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="UseTactics.html#y:44"><span class="id" title="variable">y</span></a>)<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#z:45"><span class="id" title="variable">z</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span>. <span class="id" title="var">asserts_rewrite</span> (<span class="id" title="keyword">∀</span> <a id="a:48" class="idref" href="#a:48"><span class="id" title="binder">a</span></a> <a id="b:49" class="idref" href="#b:49"><span class="id" title="binder">b</span></a>, <a class="idref" href="UseTactics.html#a:46"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">*(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="UseTactics.html#b:47"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#a:46"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="UseTactics.html#b:47"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a><a class="idref" href="UseTactics.html#a:46"><span class="id" title="variable">a</span></a>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;first&nbsp;subgoal:&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="keyword">∀</span></span> <span class="inlinecode"><span class="id" title="var">a</span></span> <span class="inlinecode"><span class="id" title="var">b</span>,</span> <span class="inlinecode"><span class="id" title="var">a</span>*(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">b</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">a</span>×<span class="id" title="var">b</span>+<span class="id" title="var">a</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;second&nbsp;subgoal:&nbsp;<span class="inlinecode">(<span class="id" title="var">u</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" title="var">v</span>)</span> <span class="inlinecode">×</span> <span class="inlinecode">(<span class="id" title="var">w</span></span> <span class="inlinecode">×</span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" title="var">y</span>)</span> <span class="inlinecode">+</span> <span class="inlinecode">(<span class="id" title="var">u</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" title="var">v</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">z</span></span>&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
<a id="lab551"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">substs</span></span></h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">substs</span></span> is similar to <span class="inlinecode"><span class="id" title="tactic">subst</span></span> except that it
    does not fail when the goal contains "circular equalities",
    such as <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="EqualityExamples.demo_substs" class="idref" href="#EqualityExamples.demo_substs"><span class="id" title="lemma">demo_substs</span></a> : <span class="id" title="keyword">∀</span> <a id="x:50" class="idref" href="#x:50"><span class="id" title="binder">x</span></a> <a id="y:51" class="idref" href="#y:51"><span class="id" title="binder">y</span></a> (<a id="f:52" class="idref" href="#f:52"><span class="id" title="binder">f</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#x:50"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#f:52"><span class="id" title="variable">f</span></a> <a class="idref" href="UseTactics.html#x:50"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#y:51"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#x:50"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#y:51"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#f:52"><span class="id" title="variable">f</span></a> <a class="idref" href="UseTactics.html#x:50"><span class="id" title="variable">x</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span>. <span class="id" title="var">substs</span>. <span class="comment">(*&nbsp;the&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" title="tactic">subst</span></span>&nbsp;would&nbsp;fail&nbsp;here&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">assumption</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab552"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">fequals</span></span></h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">fequals</span></span> is similar to <span class="inlinecode"><span class="id" title="tactic">f_equal</span></span> except that it
    directly discharges all the trivial subgoals produced. Moreover,
    the tactic <span class="inlinecode"><span class="id" title="var">fequals</span></span> features an enhanced treatment of equalities
    between tuples. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="EqualityExamples.demo_fequals" class="idref" href="#EqualityExamples.demo_fequals"><span class="id" title="lemma">demo_fequals</span></a> : <span class="id" title="keyword">∀</span> (<a id="a:53" class="idref" href="#a:53"><span class="id" title="binder">a</span></a> <a id="b:54" class="idref" href="#b:54"><span class="id" title="binder">b</span></a> <a id="c:55" class="idref" href="#c:55"><span class="id" title="binder">c</span></a> <a id="d:56" class="idref" href="#d:56"><span class="id" title="binder">d</span></a> <a id="e:57" class="idref" href="#e:57"><span class="id" title="binder">e</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="f:58" class="idref" href="#f:58"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#a:53"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#b:54"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#e:57"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#e:57"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 2 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#f:58"><span class="id" title="variable">f</span></a> <a class="idref" href="UseTactics.html#a:53"><span class="id" title="variable">a</span></a> <a class="idref" href="UseTactics.html#b:54"><span class="id" title="variable">b</span></a> <a class="idref" href="UseTactics.html#c:55"><span class="id" title="variable">c</span></a> <a class="idref" href="UseTactics.html#d:56"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#f:58"><span class="id" title="variable">f</span></a> 1 2 <a class="idref" href="UseTactics.html#c:55"><span class="id" title="variable">c</span></a> 4.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span>. <span class="id" title="var">fequals</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;subgoals&nbsp;<span class="inlinecode"><span class="id" title="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode">1</span>,&nbsp;<span class="inlinecode"><span class="id" title="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode">2</span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">c</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">c</span></span>&nbsp;are&nbsp;proved,&nbsp;<span class="inlinecode"><span class="id" title="var">d</span></span> <span class="inlinecode">=</span> <span class="inlinecode">4</span>&nbsp;remains&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
<a id="lab553"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">applys_eq</span></span></h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> is a variant of <span class="inlinecode"><span class="id" title="tactic">eapply</span></span> that introduces
    equalities for subterms that do not unify. For example, assume
    the goal is the proposition <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span> and assume we have the
    assumption <span class="inlinecode"><span class="id" title="var">H</span></span> asserting that <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">z</span></span> holds. We know that we can
    prove <span class="inlinecode"><span class="id" title="var">y</span></span> to be equal to <span class="inlinecode"><span class="id" title="var">z</span></span>. So, we could call the tactic
    <span class="inlinecode"><span class="id" title="var">assert_rewrite</span></span> <span class="inlinecode">(<span class="id" title="var">y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">z</span>)</span> and change the goal to <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">z</span></span>, but
    this would require copy-pasting the values of <span class="inlinecode"><span class="id" title="var">y</span></span> and <span class="inlinecode"><span class="id" title="var">z</span></span>.
    With the tactic <span class="inlinecode"><span class="id" title="var">applys_eq</span></span>, we can call <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode">1</span>, which
    proves the goal and leaves only the subgoal <span class="inlinecode"><span class="id" title="var">y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">z</span></span>. The value <span class="inlinecode">1</span>
    given as argument to <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> indicates that we want an equality
    to be introduced for the first argument of <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span> counting from
    the right. The three following examples illustrate the behavior
    of a call to <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode">1</span>, a call to <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode">2</span>, and a
    call to <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode">1</span> <span class="inlinecode">2</span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Axiom</span> <a id="EqualityExamples.big_expression_using" class="idref" href="#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>. <span class="comment">(*&nbsp;Used&nbsp;in&nbsp;the&nbsp;example&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="EqualityExamples.demo_applys_eq_1" class="idref" href="#EqualityExamples.demo_applys_eq_1"><span class="id" title="lemma">demo_applys_eq_1</span></a> : <span class="id" title="keyword">∀</span> (<a id="P:60" class="idref" href="#P:60"><span class="id" title="binder">P</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><span class="id" title="keyword">Prop</span>) <a id="x:61" class="idref" href="#x:61"><span class="id" title="binder">x</span></a> <a id="y:62" class="idref" href="#y:62"><span class="id" title="binder">y</span></a> <a id="z:63" class="idref" href="#z:63"><span class="id" title="binder">z</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#P:60"><span class="id" title="variable">P</span></a> <a class="idref" href="UseTactics.html#x:61"><span class="id" title="variable">x</span></a> (<a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <a class="idref" href="UseTactics.html#z:63"><span class="id" title="variable">z</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#P:60"><span class="id" title="variable">P</span></a> <a class="idref" href="UseTactics.html#x:61"><span class="id" title="variable">x</span></a> (<a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <a class="idref" href="UseTactics.html#y:62"><span class="id" title="variable">y</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> <span class="id" title="var">H</span>. <span class="id" title="var">dup</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;old&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<span class="id" title="var">Eq</span>: <a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <span class="id" title="var">z</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">admit</span>. <span class="comment">(*&nbsp;Assume&nbsp;we&nbsp;can&nbsp;prove&nbsp;this&nbsp;equality&nbsp;somehow.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">Eq</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">applys_eq</span> <span class="id" title="var">H</span> 1.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">admit</span>. <span class="comment">(*&nbsp;Assume&nbsp;we&nbsp;can&nbsp;prove&nbsp;this&nbsp;equality&nbsp;somehow.&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
If the mismatch was on the first argument of <span class="inlinecode"><span class="id" title="var">P</span></span> instead of
    the second, we would have written <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode">2</span>. Recall
    that the occurences are counted from the right. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="EqualityExamples.demo_applys_eq_2" class="idref" href="#EqualityExamples.demo_applys_eq_2"><span class="id" title="lemma">demo_applys_eq_2</span></a> : <span class="id" title="keyword">∀</span> (<a id="P:64" class="idref" href="#P:64"><span class="id" title="binder">P</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><span class="id" title="keyword">Prop</span>) <a id="x:65" class="idref" href="#x:65"><span class="id" title="binder">x</span></a> <a id="y:66" class="idref" href="#y:66"><span class="id" title="binder">y</span></a> <a id="z:67" class="idref" href="#z:67"><span class="id" title="binder">z</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#P:64"><span class="id" title="variable">P</span></a> (<a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <a class="idref" href="UseTactics.html#z:67"><span class="id" title="variable">z</span></a>) <a class="idref" href="UseTactics.html#x:65"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#P:64"><span class="id" title="variable">P</span></a> (<a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <a class="idref" href="UseTactics.html#y:66"><span class="id" title="variable">y</span></a>) <a class="idref" href="UseTactics.html#x:65"><span class="id" title="variable">x</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> <span class="id" title="var">H</span>. <span class="id" title="var">applys_eq</span> <span class="id" title="var">H</span> 2.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
When we have a mismatch on two arguments, we want to produce
    two equalities. To achieve this, we may call <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode">1</span> <span class="inlinecode">2</span>.
    More generally, the tactic <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> expects a lemma and a
    sequence of natural numbers as arguments. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="EqualityExamples.demo_applys_eq_3" class="idref" href="#EqualityExamples.demo_applys_eq_3"><span class="id" title="lemma">demo_applys_eq_3</span></a> : <span class="id" title="keyword">∀</span> (<a id="P:68" class="idref" href="#P:68"><span class="id" title="binder">P</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><span class="id" title="keyword">Prop</span>) <a id="x<sub>1</sub>:69" class="idref" href="#x<sub>1</sub>:69"><span class="id" title="binder">x<sub>1</sub></span></a> <a id="x<sub>2</sub>:70" class="idref" href="#x<sub>2</sub>:70"><span class="id" title="binder">x<sub>2</sub></span></a> <a id="y<sub>1</sub>:71" class="idref" href="#y<sub>1</sub>:71"><span class="id" title="binder">y<sub>1</sub></span></a> <a id="y<sub>2</sub>:72" class="idref" href="#y<sub>2</sub>:72"><span class="id" title="binder">y<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#P:68"><span class="id" title="variable">P</span></a> (<a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <a class="idref" href="UseTactics.html#x<sub>2</sub>:70"><span class="id" title="variable">x<sub>2</sub></span></a>) (<a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <a class="idref" href="UseTactics.html#y<sub>2</sub>:72"><span class="id" title="variable">y<sub>2</sub></span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#P:68"><span class="id" title="variable">P</span></a> (<a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <a class="idref" href="UseTactics.html#x<sub>1</sub>:69"><span class="id" title="variable">x<sub>1</sub></span></a>) (<a class="idref" href="UseTactics.html#EqualityExamples.big_expression_using"><span class="id" title="axiom">big_expression_using</span></a> <a class="idref" href="UseTactics.html#y<sub>1</sub>:71"><span class="id" title="variable">y<sub>1</sub></span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> <span class="id" title="var">H</span>. <span class="id" title="var">applys_eq</span> <span class="id" title="var">H</span> 1 2.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;produces&nbsp;two&nbsp;subgoals:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">big_expression_using</span></span> <span class="inlinecode"><span class="id" title="var">x<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">big_expression_using</span></span> <span class="inlinecode"><span class="id" title="var">x<sub>2</sub></span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">big_expression_using</span></span> <span class="inlinecode"><span class="id" title="var">y<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">big_expression_using</span></span> <span class="inlinecode"><span class="id" title="var">y<sub>2</sub></span></span>&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#EqualityExamples"><span class="id" title="module">EqualityExamples</span></a>.<br/>
</div>

<div class="doc">
<a id="lab554"></a><h1 class="section">Some Convenient Shorthands</h1>

<div class="paragraph"> </div>

 This section of the tutorial introduces a few tactics
    that help make proof scripts shorter and more readable:
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">unfolds</span></span> (without argument) for unfolding the head definition,

</li>
<li> <span class="inlinecode"><span class="id" title="var">false</span></span> for replacing the goal with <span class="inlinecode"><span class="id" title="var">False</span></span>,

</li>
<li> <span class="inlinecode"><span class="id" title="var">gen</span></span> as a shorthand for <span class="inlinecode"><span class="id" title="tactic">dependent</span></span> <span class="inlinecode"><span class="id" title="tactic">generalize</span></span>,

</li>
<li> <span class="inlinecode"><span class="id" title="var">admits</span></span> for naming an addmited fact,

</li>
<li> <span class="inlinecode"><span class="id" title="var">admit_rewrite</span></span> for rewriting using an admitted equality,

</li>
<li> <span class="inlinecode"><span class="id" title="var">admit_goal</span></span> to set up a proof by induction by skipping the
      justification that some order decreases,

</li>
<li> <span class="inlinecode"><span class="id" title="var">sort</span></span> for re-ordering the proof context by moving moving all
      propositions at the bottom. 
</li>
</ul>

</div>

<div class="doc">
<a id="lab555"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">unfolds</span></span></h2>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="UnfoldsExample" class="idref" href="#UnfoldsExample"><span class="id" title="module">UnfoldsExample</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">Hoare</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">unfolds</span></span> (without any argument) unfolds the
    head constant of the goal. This tactic saves the need to
    name the constant explicitly. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="UnfoldsExample.bexp_eval_true" class="idref" href="#UnfoldsExample.bexp_eval_true"><span class="id" title="lemma">bexp_eval_true</span></a> : <span class="id" title="keyword">∀</span> <a id="b:73" class="idref" href="#b:73"><span class="id" title="binder">b</span></a> <a id="st:74" class="idref" href="#st:74"><span class="id" title="binder">st</span></a>,<br/>
&nbsp;&nbsp;<span class="id" title="definition">beval</span> <a class="idref" href="UseTactics.html#st:74"><span class="id" title="variable">st</span></a> <a class="idref" href="UseTactics.html#b:73"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">true</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;(<a class="idref" href="Hoare.html#bassn"><span class="id" title="definition">bassn</span></a> <a class="idref" href="UseTactics.html#b:73"><span class="id" title="variable">b</span></a>) <a class="idref" href="UseTactics.html#st:74"><span class="id" title="variable">st</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">b</span> <span class="id" title="var">st</span> <span class="id" title="var">Hbe</span>. <span class="id" title="var">dup</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;old&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">unfold</span> <a class="idref" href="Hoare.html#bassn"><span class="id" title="definition">bassn</span></a>. <span class="id" title="tactic">assumption</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">unfolds</span>. <span class="id" title="tactic">assumption</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Remark: contrary to the tactic <span class="inlinecode"><span class="id" title="tactic">hnf</span></span>, which may unfold several
    constants, <span class="inlinecode"><span class="id" title="var">unfolds</span></span> performs only a single step of unfolding. 
<div class="paragraph"> </div>

 Remark: the tactic <span class="inlinecode"><span class="id" title="var">unfolds</span></span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> can be used to unfold the
    head definition of the hypothesis <span class="inlinecode"><span class="id" title="var">H</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#UnfoldsExample"><span class="id" title="module">UnfoldsExample</span></a>.<br/>
</div>

<div class="doc">
<a id="lab556"></a><h2 class="section">The Tactics <span class="inlinecode"><span class="id" title="var">false</span></span> and <span class="inlinecode"><span class="id" title="var">tryfalse</span></span></h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">false</span></span> can be used to replace any goal with <span class="inlinecode"><span class="id" title="var">False</span></span>.
    In short, it is a shorthand for <span class="inlinecode"><span class="id" title="var">exfalso</span></span>.
    Moreover, <span class="inlinecode"><span class="id" title="var">false</span></span> proves the goal if it contains an absurd
    assumption, such as <span class="inlinecode"><span class="id" title="var">False</span></span> or <span class="inlinecode">0</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span>, or if it contains
    contradictory assumptions, such as <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">true</span></span> and <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">false</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="demo_false" class="idref" href="#demo_false"><span class="id" title="lemma">demo_false</span></a> : <span class="id" title="keyword">∀</span> <a id="n:75" class="idref" href="#n:75"><span class="id" title="binder">n</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="UseTactics.html#n:75"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#n:75"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="var">false</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">false</span></span> can be given an argument: <span class="inlinecode"><span class="id" title="var">false</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> replace
    the goals with <span class="inlinecode"><span class="id" title="var">False</span></span> and then applies <span class="inlinecode"><span class="id" title="var">H</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="demo_false_arg" class="idref" href="#demo_false_arg"><span class="id" title="lemma">demo_false_arg</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <a id="n:76" class="idref" href="#n:76"><span class="id" title="binder">n</span></a>, <a class="idref" href="UseTactics.html#n:76"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&lt;'_x"><span class="id" title="notation">&lt;</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#False"><span class="id" title="inductive">False</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;3 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&lt;'_x"><span class="id" title="notation">&lt;</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;4 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&lt;'_x"><span class="id" title="notation">&lt;</span></a> 0.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">H</span> <span class="id" title="var">L</span>. <span class="id" title="var">false</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">L</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">tryfalse</span></span> is a shorthand for <span class="inlinecode"><span class="id" title="tactic">try</span></span> <span class="inlinecode"><span class="id" title="tactic">solve</span></span> <span class="inlinecode">[<span class="id" title="var">false</span>]</span>:
    it tries to find a contradiction in the goal. The tactic
    <span class="inlinecode"><span class="id" title="var">tryfalse</span></span> is generally called after a case analysis. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="demo_tryfalse" class="idref" href="#demo_tryfalse"><span class="id" title="lemma">demo_tryfalse</span></a> : <span class="id" title="keyword">∀</span> <a id="n:77" class="idref" href="#n:77"><span class="id" title="binder">n</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="UseTactics.html#n:77"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#n:77"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span>; <span class="id" title="var">tryfalse</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab557"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">gen</span></span></h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" title="var">gen</span></span> is a shortand for <span class="inlinecode"><span class="id" title="tactic">generalize</span></span> <span class="inlinecode"><span class="id" title="tactic">dependent</span></span>
    that accepts several arguments at once. An invocation of
    this tactic takes the form <span class="inlinecode"><span class="id" title="var">gen</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span> <span class="inlinecode"><span class="id" title="var">z</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="GenExample" class="idref" href="#GenExample"><span class="id" title="module">GenExample</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">Stlc</span>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">STLC</span>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">Maps</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="GenExample.substitution_preserves_typing" class="idref" href="#GenExample.substitution_preserves_typing"><span class="id" title="lemma">substitution_preserves_typing</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:78" class="idref" href="#Gamma:78"><span class="id" title="binder">Gamma</span></a> <a id="x:79" class="idref" href="#x:79"><span class="id" title="binder">x</span></a> <a id="U:80" class="idref" href="#U:80"><span class="id" title="binder">U</span></a> <a id="t:81" class="idref" href="#t:81"><span class="id" title="binder">t</span></a> <a id="v:82" class="idref" href="#v:82"><span class="id" title="binder">v</span></a> <a id="T:83" class="idref" href="#T:83"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#x:79"><span class="id" title="variable">x</span></a> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="UseTactics.html#U:80"><span class="id" title="variable">U</span></a> <span class="id" title="notation">;</span> <a class="idref" href="UseTactics.html#Gamma:78"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="UseTactics.html#t:81"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="UseTactics.html#T:83"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="UseTactics.html#v:82"><span class="id" title="variable">v</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="UseTactics.html#U:80"><span class="id" title="variable">U</span></a>   <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#Gamma:78"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">[</span></a><a class="idref" href="UseTactics.html#x:79"><span class="id" title="variable">x</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">:=</span></a><a class="idref" href="UseTactics.html#v:82"><span class="id" title="variable">v</span></a><a class="idref" href="Stlc.html#af81635d67c091f2566d9a89993ee012"><span class="id" title="notation">]</span></a><a class="idref" href="UseTactics.html#t:81"><span class="id" title="variable">t</span></a> <a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Stlc.html#092ca644792e367ec17fc46e3cfd4c<sub>33</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="UseTactics.html#T:83"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">dup</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;old&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">x</span> <span class="id" title="var">U</span> <span class="id" title="var">t</span> <span class="id" title="var">v</span> <span class="id" title="var">T</span> <span class="id" title="var">Ht</span> <span class="id" title="var">Hv</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma</span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">t</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">T</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">admit</span>. <span class="id" title="var">admit</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" title="var">introv</span> <span class="id" title="var">Ht</span> <span class="id" title="var">Hv</span>. <span class="id" title="var">gen</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">t</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">S</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">admit</span>. <span class="id" title="var">admit</span>.<br/>
<span class="id" title="keyword">Abort</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#GenExample"><span class="id" title="module">GenExample</span></a>.<br/>
</div>

<div class="doc">
<a id="lab558"></a><h2 class="section">The Tactics <span class="inlinecode"><span class="id" title="var">admits</span></span>, <span class="inlinecode"><span class="id" title="var">admit_rewrite</span></span> and <span class="inlinecode"><span class="id" title="var">admit_goal</span></span></h2>

<div class="paragraph"> </div>

 Temporarily admitting a given subgoal is very useful when
    constructing proofs. Several tactics are provided as
    useful wrappers around the builtin <span class="inlinecode"><span class="id" title="var">admit</span></span> tactic. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="SkipExample" class="idref" href="#SkipExample"><span class="id" title="module">SkipExample</span></a>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">admits</span></span> <span class="inlinecode"><span class="id" title="var">H</span>:</span> <span class="inlinecode"><span class="id" title="var">P</span></span> adds the hypothesis <span class="inlinecode"><span class="id" title="var">H</span>:</span> <span class="inlinecode"><span class="id" title="var">P</span></span> to the context,
    without checking whether the proposition <span class="inlinecode"><span class="id" title="var">P</span></span> is true.
    It is useful for exploiting a fact and postponing its proof.
    Note: <span class="inlinecode"><span class="id" title="var">admits</span></span> <span class="inlinecode"><span class="id" title="var">H</span>:</span> <span class="inlinecode"><span class="id" title="var">P</span></span> is simply a shorthand for <span class="inlinecode"><span class="id" title="tactic">assert</span></span> <span class="inlinecode">(<span class="id" title="var">H</span>:<span class="id" title="var">P</span>).</span> <span class="inlinecode"><span class="id" title="var">admit</span>.</span> 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="SkipExample.demo_admits" class="idref" href="#SkipExample.demo_admits"><span class="id" title="lemma">demo_admits</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">admits</span> <span class="id" title="var">H</span>: (<span class="id" title="keyword">∀</span> <a id="n:86" class="idref" href="#n:86"><span class="id" title="binder">n</span></a> <a id="m:87" class="idref" href="#m:87"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">(</span></a>0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="UseTactics.html#n:84"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#m:85"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#n:84"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#m:85"><span class="id" title="variable">m</span></a>).<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">admit_rewrite</span></span> <span class="inlinecode">(<span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span>)</span> replaces <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> with <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span> in
    the goal, without checking that <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> is actually equal to <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="SkipExample.mult_plus_0" class="idref" href="#SkipExample.mult_plus_0"><span class="id" title="lemma">mult_plus_0</span></a> : <span class="id" title="keyword">∀</span> <a id="n:88" class="idref" href="#n:88"><span class="id" title="binder">n</span></a> <a id="m:89" class="idref" href="#m:89"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="UseTactics.html#n:88"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 0<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#m:89"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#n:88"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="UseTactics.html#m:89"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">dup</span> 3.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;old&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<span class="id" title="var">H</span>: <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">n</span>). <span class="id" title="var">admit</span>. <span class="id" title="tactic">rewrite</span> → <span class="id" title="var">H</span>. <span class="id" title="tactic">clear</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">admit_rewrite</span> (<span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">n</span>).<br/>
&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Remark:&nbsp;<span class="inlinecode"><span class="id" title="var">admit_rewrite</span></span>&nbsp;can&nbsp;be&nbsp;given&nbsp;a&nbsp;lemma&nbsp;statement&nbsp;as&nbsp;argument,<br/>
&nbsp;&nbsp;&nbsp;like&nbsp;<span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span>.&nbsp;For&nbsp;example:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">admit_rewrite</span> (<span class="id" title="keyword">∀</span> <a id="a:91" class="idref" href="#a:91"><span class="id" title="binder">a</span></a>, <a class="idref" href="UseTactics.html#a:90"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#a:90"><span class="id" title="variable">a</span></a>).<br/>
&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">admit_goal</span></span> adds the current goal as hypothesis.
    This cheat is useful to set up the structure of a proof by
    induction without having to worry about the induction hypothesis
    being applied only to smaller arguments. Using <span class="inlinecode"><span class="id" title="var">skip_goal</span></span>, one
    can construct a proof in two steps: first, check that the main
    arguments go through without waisting time on fixing the details
    of the induction hypotheses; then, focus on fixing the invokations
    of the induction hypothesis. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="SkipExample.ceval_deterministic" class="idref" href="#SkipExample.ceval_deterministic"><span class="id" title="lemma">ceval_deterministic</span></a>: <span class="id" title="keyword">∀</span> <a id="c:92" class="idref" href="#c:92"><span class="id" title="binder">c</span></a> <a id="st:93" class="idref" href="#st:93"><span class="id" title="binder">st</span></a> <a id="st<sub>1</sub>:94" class="idref" href="#st<sub>1</sub>:94"><span class="id" title="binder">st<sub>1</sub></span></a> <a id="st<sub>2</sub>:95" class="idref" href="#st<sub>2</sub>:95"><span class="id" title="binder">st<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:93"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:92"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>1</sub>:94"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:93"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:92"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>2</sub>:95"><span class="id" title="variable">st<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st<sub>1</sub>:94"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#st<sub>2</sub>:95"><span class="id" title="variable">st<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" title="var">admit_goal</span></span>&nbsp;creates&nbsp;an&nbsp;hypothesis&nbsp;called&nbsp;<span class="inlinecode"><span class="id" title="var">IH</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;asserting&nbsp;that&nbsp;the&nbsp;statment&nbsp;of&nbsp;<span class="inlinecode"><span class="id" title="var">ceval_deterministic</span></span>&nbsp;is&nbsp;true.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">admit_goal</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Of&nbsp;course,&nbsp;if&nbsp;we&nbsp;call&nbsp;<span class="inlinecode"><span class="id" title="tactic">assumption</span></span>&nbsp;here,&nbsp;then&nbsp;the&nbsp;goal&nbsp;is&nbsp;solved<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;right&nbsp;away,&nbsp;but&nbsp;the&nbsp;point&nbsp;is&nbsp;to&nbsp;do&nbsp;the&nbsp;proof&nbsp;and&nbsp;use&nbsp;<span class="inlinecode"><span class="id" title="var">IH</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;only&nbsp;at&nbsp;the&nbsp;places&nbsp;where&nbsp;we&nbsp;need&nbsp;an&nbsp;induction&nbsp;hypothesis.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">introv</span> <span class="id" title="var">E<sub>1</sub></span> <span class="id" title="var">E<sub>2</sub></span>. <span class="id" title="var">gen</span> <span class="id" title="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">E<sub>1</sub></span>; <span class="id" title="var">introv</span> <span class="id" title="var">E<sub>2</sub></span>; <span class="id" title="var">inverts</span> <span class="id" title="var">E<sub>2</sub></span> <span class="id" title="keyword">as</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Skip&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Ass&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">subst</span> <span class="id" title="var">n</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Seq&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">st<sub>3</sub></span> <span class="id" title="var">Red1</span> <span class="id" title="var">Red2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<span class="id" title="var">st'</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">st<sub>3</sub></span>) <span class="id" title="keyword">as</span> <span class="id" title="var">EQ<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;Proof&nbsp;of&nbsp;assertion&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;was:&nbsp;<span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="var">IHE1_1</span>;</span> <span class="inlinecode"><span class="id" title="tactic">assumption</span>.</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;*)</span> <span class="id" title="tactic">eapply</span> <span class="id" title="var">IH</span>. <span class="id" title="tactic">eapply</span> <span class="id" title="var">E1_1</span>. <span class="id" title="tactic">eapply</span> <span class="id" title="var">Red1</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">subst</span> <span class="id" title="var">st<sub>3</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;was:&nbsp;apply&nbsp;IHE1_2.&nbsp;assumption.]&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;*)</span> <span class="id" title="tactic">eapply</span> <span class="id" title="var">IH</span>. <span class="id" title="tactic">eapply</span> <span class="id" title="var">E1_2</span>. <span class="id" title="tactic">eapply</span> <span class="id" title="var">Red2</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;other&nbsp;cases&nbsp;are&nbsp;similiar.&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#SkipExample"><span class="id" title="module">SkipExample</span></a>.<br/>
</div>

<div class="doc">
<a id="lab559"></a><h2 class="section">The Tactic <span class="inlinecode"><span class="id" title="var">sort</span></span></h2>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="SortExamples" class="idref" href="#SortExamples"><span class="id" title="module">SortExamples</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">Imp</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" title="var">sort</span></span> reorganizes the proof context by placing
    all the variables at the top and all the hypotheses at the
    bottom, thereby making the proof context more readable. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="SortExamples.ceval_deterministic" class="idref" href="#SortExamples.ceval_deterministic"><span class="id" title="lemma">ceval_deterministic</span></a>: <span class="id" title="keyword">∀</span> <a id="c:96" class="idref" href="#c:96"><span class="id" title="binder">c</span></a> <a id="st:97" class="idref" href="#st:97"><span class="id" title="binder">st</span></a> <a id="st<sub>1</sub>:98" class="idref" href="#st<sub>1</sub>:98"><span class="id" title="binder">st<sub>1</sub></span></a> <a id="st<sub>2</sub>:99" class="idref" href="#st<sub>2</sub>:99"><span class="id" title="binder">st<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:97"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:96"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>1</sub>:98"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st:97"><span class="id" title="variable">st</span></a> <span class="id" title="notation">=[</span> <a class="idref" href="UseTactics.html#c:96"><span class="id" title="variable">c</span></a> <span class="id" title="notation">]=&gt;</span> <a class="idref" href="UseTactics.html#st<sub>2</sub>:99"><span class="id" title="variable">st<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#st<sub>1</sub>:98"><span class="id" title="variable">st<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="UseTactics.html#st<sub>2</sub>:99"><span class="id" title="variable">st<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">c</span> <span class="id" title="var">st</span> <span class="id" title="var">st<sub>1</sub></span> <span class="id" title="var">st<sub>2</sub></span> <span class="id" title="var">E<sub>1</sub></span> <span class="id" title="var">E<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">E<sub>1</sub></span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">st<sub>2</sub></span> <span class="id" title="var">E<sub>2</sub></span>; <span class="id" title="var">inverts</span> <span class="id" title="var">E<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">admit</span>. <span class="id" title="var">admit</span>. <span class="comment">(*&nbsp;Skipping&nbsp;some&nbsp;trivial&nbsp;cases&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">sort</span>. <span class="comment">(*&nbsp;Observe&nbsp;how&nbsp;the&nbsp;context&nbsp;is&nbsp;reorganized&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#SortExamples"><span class="id" title="module">SortExamples</span></a>.<br/>
</div>

<div class="doc">
<a id="lab560"></a><h1 class="section">Tactics for Advanced Lemma Instantiation</h1>

<div class="paragraph"> </div>

 This last section describes a mechanism for instantiating a lemma
    by providing some of its arguments and leaving other implicit.
    Variables whose instantiation is not provided are turned into
    existentential variables, and facts whose instantiation is not
    provided are turned into subgoals.

<div class="paragraph"> </div>

    Remark: this instantion mechanism goes far beyond the abilities of
    the "Implicit Arguments" mechanism. The point of the instantiation
    mechanism described in this section is that you will no longer need
    to spend time figuring out how many underscore symbols you need to
    write. 
<div class="paragraph"> </div>

 In this section, we'll use a useful feature of Coq for decomposing
    conjunctions and existentials. In short, a tactic like <span class="inlinecode"><span class="id" title="tactic">intros</span></span> or
    <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> can be provided with a pattern <span class="inlinecode">(<span class="id" title="var">H<sub>1</sub></span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">H<sub>2</sub></span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">H<sub>3</sub></span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">H<sub>4</sub></span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">H<sub>5</sub></span>)</span>,
    which is a shorthand for <span class="inlinecode">[<span class="id" title="var">H<sub>1</sub></span></span> <span class="inlinecode">[<span class="id" title="var">H<sub>2</sub></span></span> <span class="inlinecode">[<span class="id" title="var">H<sub>3</sub></span></span> <span class="inlinecode">[<span class="id" title="var">H<sub>4</sub></span></span> <span class="inlinecode"><span class="id" title="var">H<sub>5</sub></span>]]]]</span>]. For example,
    <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> <span class="inlinecode">(<span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">Htypt</span>)</span> <span class="inlinecode"><span class="id" title="keyword">as</span></span> <span class="inlinecode">[<span class="id" title="var">T</span></span> <span class="inlinecode">[<span class="id" title="var">Hctx</span></span> <span class="inlinecode"><span class="id" title="var">Hsub</span>]].</span> can be rewritten in
    the form <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> <span class="inlinecode">(<span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">Htypt</span>)</span> <span class="inlinecode"><span class="id" title="keyword">as</span></span> <span class="inlinecode">(<span class="id" title="var">T</span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">Hctx</span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">Hsub</span>).</span> 
</div>

<div class="doc">
<a id="lab561"></a><h2 class="section">Working of <span class="inlinecode"><span class="id" title="var">lets</span></span></h2>

<div class="paragraph"> </div>

 When we have a lemma (or an assumption) that we want to exploit,
    we often need to explicitly provide arguments to this lemma,
    writing something like:
    <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> <span class="inlinecode">(<span class="id" title="var">typing_inversion_var</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span> <span class="inlinecode"><span class="id" title="var">Htypt</span>)</span> <span class="inlinecode"><span class="id" title="keyword">as</span></span> <span class="inlinecode">(<span class="id" title="var">T</span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">Hctx</span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">Hsub</span>).</span>
    The need to write several times the "underscore" symbol is tedious.
    Not only we need to figure out how many of them to write down, but
    it also makes the proof scripts look prettly ugly. With the tactic
    <span class="inlinecode"><span class="id" title="var">lets</span></span>, one can simply write:
    <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode">(<span class="id" title="var">T</span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">Hctx</span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">Hsub</span>):</span> <span class="inlinecode"><span class="id" title="var">typing_inversion_var</span></span> <span class="inlinecode"><span class="id" title="var">Htypt</span>.</span>

<div class="paragraph"> </div>

    In short, this tactic <span class="inlinecode"><span class="id" title="var">lets</span></span> allows to specialize a lemma on a bunch
    of variables and hypotheses. The syntax is <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode"><span class="id" title="var">I</span>:</span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode">..</span> <span class="inlinecode"><span class="id" title="var">EN</span></span>,
    for building an hypothesis named <span class="inlinecode"><span class="id" title="var">I</span></span> by applying the fact <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> to the
    arguments <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> to <span class="inlinecode"><span class="id" title="var">EN</span></span>. Not all the arguments need to be provided,
    however the arguments that are provided need to be provided in the
    correct order. The tactic relies on a first-match algorithm based on
    types in order to figure out how the to instantiate the lemma with
    the arguments provided. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Module</span> <a id="ExamplesLets" class="idref" href="#ExamplesLets"><span class="id" title="module">ExamplesLets</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="var">Sub</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;To&nbsp;illustrate&nbsp;the&nbsp;working&nbsp;of&nbsp;<span class="inlinecode"><span class="id" title="var">lets</span></span>,&nbsp;assume&nbsp;that&nbsp;we&nbsp;want&nbsp;to<br/>
&nbsp;&nbsp;&nbsp;exploit&nbsp;the&nbsp;following&nbsp;lemma.&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Maps</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">Sub</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">String</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Axiom</span> <a id="ExamplesLets.typing_inversion_var" class="idref" href="#ExamplesLets.typing_inversion_var"><span class="id" title="axiom">typing_inversion_var</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:100" class="idref" href="#Gamma:100"><span class="id" title="binder">Gamma</span></a> (<a id="x:101" class="idref" href="#x:101"><span class="id" title="binder">x</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) <a id="T:102" class="idref" href="#T:102"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#Gamma:100"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Sub.html#3b5796de2387691122e67a3516cd710b"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="UseTactics.html#x:101"><span class="id" title="variable">x</span></a> <a class="idref" href="Sub.html#3b5796de2387691122e67a3516cd710b"><span class="id" title="notation">\</span></a><a class="idref" href="Sub.html#3b5796de2387691122e67a3516cd710b"><span class="id" title="notation">in</span></a> <a class="idref" href="UseTactics.html#T:102"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="S:103" class="idref" href="#S:103"><span class="id" title="binder">S</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="UseTactics.html#Gamma:100"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="UseTactics.html#x:101"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="UseTactics.html#S:103"><span class="id" title="variable">S</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="UseTactics.html#S:103"><span class="id" title="variable">S</span></a> <a class="idref" href="Sub.html#:::x_'&lt;:'_x"><span class="id" title="notation">&lt;:</span></a> <a class="idref" href="UseTactics.html#T:102"><span class="id" title="variable">T</span></a>.<br/>
</div>

<div class="doc">
First, assume we have an assumption <span class="inlinecode"><span class="id" title="var">H</span></span> with the type of the form
    <span class="inlinecode"><span class="id" title="var">has_type</span></span> <span class="inlinecode"><span class="id" title="var">G</span></span> <span class="inlinecode">(<span class="id" title="var">var</span></span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">T</span></span>. We can obtain the conclusion of the
    lemma <span class="inlinecode"><span class="id" title="var">typing_inversion_var</span></span> by invoking the tactics
    <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode"><span class="id" title="var">K</span>:</span> <span class="inlinecode"><span class="id" title="var">typing_inversion_var</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>, as shown next. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="ExamplesLets.demo_lets_1" class="idref" href="#ExamplesLets.demo_lets_1"><span class="id" title="lemma">demo_lets_1</span></a> : <span class="id" title="keyword">∀</span> (<a id="G:105" class="idref" href="#G:105"><span class="id" title="binder">G</span></a>:<a class="idref" href="Sub.html#context"><span class="id" title="definition">context</span></a>) (<a id="x:106" class="idref" href="#x:106"><span class="id" title="binder">x</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="T:107" class="idref" href="#T:107"><span class="id" title="binder">T</span></a>:<a class="idref" href="Sub.html#ty"><span class="id" title="inductive">ty</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="UseTactics.html#G:105"><span class="id" title="variable">G</span></a> <a class="idref" href="Sub.html#3b5796de2387691122e67a3516cd710b"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="UseTactics.html#x:106"><span class="id" title="variable">x</span></a> <a class="idref" href="Sub.html#3b5796de2387691122e67a3516cd710b"><span class="id" title="notation">\</span></a><a class="idref" href="Sub.html#3b5796de2387691122e67a3516cd710b"><span class="id" title="notation">in</span></a> <a class="idref" href="UseTactics.html#T:107"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">G</span> <span class="id" title="var">x</span> <span class="id" title="var">T</span> <span class="id" title="var">H</span>. <span class="id" title="var">dup</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;step-by-step:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">lets</span> <span class="id" title="var">K</span>: <a class="idref" href="UseTactics.html#ExamplesLets.typing_inversion_var"><span class="id" title="axiom">typing_inversion_var</span></a> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">K</span> <span class="id" title="keyword">as</span> (<span class="id" title="var">S</span> &amp; <span class="id" title="var">Eq</span> &amp; <span class="id" title="var">Sub</span>).<br/>
&nbsp;&nbsp;<span class="id" title="var">admit</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;all-at-once:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">lets</span> (<span class="id" title="var">S</span> &amp; <span class="id" title="var">Eq</span> &amp; <span class="id" title="var">Sub</span>): <a class="idref" href="UseTactics.html#ExamplesLets.typing_inversion_var"><span class="id" title="axiom">typing_inversion_var</span></a> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">admit</span>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
Assume now that we know the values of <span class="inlinecode"><span class="id" title="var">G</span></span>, <span class="inlinecode"><span class="id" title="var">x</span></span> and <span class="inlinecode"><span class="id" title="var">T</span></span> and we
    want to obtain <span class="inlinecode"><span class="id" title="var">S</span></span>, and have <span class="inlinecode"><span class="id" title="var">has_type</span></span> <span class="inlinecode"><span class="id" title="var">G</span></span> <span class="inlinecode">(<span class="id" title="var">var</span></span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">T</span></span> be produced
    as a subgoal. To indicate that we want all the remaining arguments
    of <span class="inlinecode"><span class="id" title="var">typing_inversion_var</span></span> to be produced as subgoals, we use a
    triple-underscore symbol <span class="inlinecode"><span class="id" title="var">___</span></span>. (We'll later introduce a shorthand
    tactic called <span class="inlinecode"><span class="id" title="var">forwards</span></span> to avoid writing triple underscores.) 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="ExamplesLets.demo_lets_2" class="idref" href="#ExamplesLets.demo_lets_2"><span class="id" title="lemma">demo_lets_2</span></a> : <span class="id" title="keyword">∀</span> (<a id="G:108" class="idref" href="#G:108"><span class="id" title="binder">G</span></a>:<a class="idref" href="Sub.html#context"><span class="id" title="definition">context</span></a>) (<a id="x:109" class="idref" href="#x:109"><span class="id" title="binder">x</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="T:110" class="idref" href="#T:110"><span class="id" title="binder">T</span></a>:<a class="idref" href="Sub.html#ty"><span class="id" title="inductive">ty</span></a>), <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">G</span> <span class="id" title="var">x</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">lets</span> (<span class="id" title="var">S</span> &amp; <span class="id" title="var">Eq</span> &amp; <span class="id" title="var">Sub</span>): <a class="idref" href="UseTactics.html#ExamplesLets.typing_inversion_var"><span class="id" title="axiom">typing_inversion_var</span></a> <span class="id" title="var">G</span> <span class="id" title="var">x</span> <span class="id" title="var">T</span> <a class="idref" href="LibTactics.html#::ltac_scope:'___'"><span class="id" title="notation">___</span></a>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
Usually, there is only one context <span class="inlinecode"><span class="id" title="var">G</span></span> and one type <span class="inlinecode"><span class="id" title="var">T</span></span> that are
    going to be suitable for proving <span class="inlinecode"><span class="id" title="var">has_type</span></span> <span class="inlinecode"><span class="id" title="var">G</span></span> <span class="inlinecode">(<span class="id" title="var">tm_var</span></span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode"><span class="id" title="var">T</span></span>, so
    we don't really need to bother giving <span class="inlinecode"><span class="id" title="var">G</span></span> and <span class="inlinecode"><span class="id" title="var">T</span></span> explicitly.
    It suffices to call <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">Eq</span></span> <span class="inlinecode">&amp;</span> <span class="inlinecode"><span class="id" title="var">Sub</span>):</span> <span class="inlinecode"><span class="id" title="var">typing_inversion_var</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span>.
    The variables <span class="inlinecode"><span class="id" title="var">G</span></span> and <span class="inlinecode"><span class="id" title="var">T</span></span> are then instantiated using existential
    variables. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="ExamplesLets.demo_lets_3" class="idref" href="#ExamplesLets.demo_lets_3"><span class="id" title="lemma">demo_lets_3</span></a> : <span class="id" title="keyword">∀</span> (<a id="x:111" class="idref" href="#x:111"><span class="id" title="binder">x</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>), <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">x</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">lets</span> (<span class="id" title="var">S</span> &amp; <span class="id" title="var">Eq</span> &amp; <span class="id" title="var">Sub</span>): <a class="idref" href="UseTactics.html#ExamplesLets.typing_inversion_var"><span class="id" title="axiom">typing_inversion_var</span></a> <span class="id" title="var">x</span> <a class="idref" href="LibTactics.html#::ltac_scope:'___'"><span class="id" title="notation">___</span></a>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
We may go even further by not giving any argument to instantiate
    <span class="inlinecode"><span class="id" title="var">typing_inversion_var</span></span>. In this case, three unification variables
    are introduced. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="ExamplesLets.demo_lets_4" class="idref" href="#ExamplesLets.demo_lets_4"><span class="id" title="lemma">demo_lets_4</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">lets</span> (<span class="id" title="var">S</span> &amp; <span class="id" title="var">Eq</span> &amp; <span class="id" title="var">Sub</span>): <a class="idref" href="UseTactics.html#ExamplesLets.typing_inversion_var"><span class="id" title="axiom">typing_inversion_var</span></a> <a class="idref" href="LibTactics.html#::ltac_scope:'___'"><span class="id" title="notation">___</span></a>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
Note: if we provide <span class="inlinecode"><span class="id" title="var">lets</span></span> with only the name of the lemma as
    argument, it simply adds this lemma in the proof context, without
    trying to instantiate any of its arguments. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="ExamplesLets.demo_lets_5" class="idref" href="#ExamplesLets.demo_lets_5"><span class="id" title="lemma">demo_lets_5</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">lets</span> <span class="id" title="var">H</span>: <a class="idref" href="UseTactics.html#ExamplesLets.typing_inversion_var"><span class="id" title="axiom">typing_inversion_var</span></a>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
A last useful feature of <span class="inlinecode"><span class="id" title="var">lets</span></span> is the double-underscore symbol,
    which allows skipping an argument when several arguments have
    the same type. In the following example, our assumption quantifies
    over two variables <span class="inlinecode"><span class="id" title="var">n</span></span> and <span class="inlinecode"><span class="id" title="var">m</span></span>, both of type <span class="inlinecode"><span class="id" title="var">nat</span></span>. We would like
    <span class="inlinecode"><span class="id" title="var">m</span></span> to be instantiated as the value <span class="inlinecode">3</span>, but without specifying a
    value for <span class="inlinecode"><span class="id" title="var">n</span></span>. This can be achieved by writting <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode"><span class="id" title="var">K</span>:</span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="var">__</span></span> <span class="inlinecode">3</span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="ExamplesLets.demo_lets_underscore" class="idref" href="#ExamplesLets.demo_lets_underscore"><span class="id" title="lemma">demo_lets_underscore</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <a id="n:112" class="idref" href="#n:112"><span class="id" title="binder">n</span></a> <a id="m:113" class="idref" href="#m:113"><span class="id" title="binder">m</span></a>, <a class="idref" href="UseTactics.html#n:112"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a<sub>3</sub>"><span class="id" title="notation">≤</span></a> <a class="idref" href="UseTactics.html#m:113"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="UseTactics.html#n:112"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#::nat_scope:x_'&lt;'_x"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="UseTactics.html#m:113"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a>1<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;we&nbsp;do&nbsp;not&nbsp;use&nbsp;a&nbsp;double&nbsp;underscore,&nbsp;the&nbsp;first&nbsp;argument,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;which&nbsp;is&nbsp;<span class="inlinecode"><span class="id" title="var">n</span></span>,&nbsp;gets&nbsp;instantiated&nbsp;as&nbsp;3.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">lets</span> <span class="id" title="var">K</span>: <span class="id" title="var">H</span> 3. <span class="comment">(*&nbsp;gives&nbsp;<span class="inlinecode"><span class="id" title="var">K</span></span>&nbsp;of&nbsp;type&nbsp;<span class="inlinecode"><span class="id" title="keyword">∀</span></span> <span class="inlinecode"><span class="id" title="var">m</span>,</span> <span class="inlinecode">3</span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode">→</span> <span class="inlinecode">3</span> <span class="inlinecode">&lt;</span> <span class="inlinecode"><span class="id" title="var">m</span>+1</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">clear</span> <span class="id" title="var">K</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;double&nbsp;underscore&nbsp;preceeding&nbsp;<span class="inlinecode">3</span>&nbsp;indicates&nbsp;that&nbsp;we&nbsp;want<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;to&nbsp;skip&nbsp;a&nbsp;value&nbsp;that&nbsp;has&nbsp;the&nbsp;type&nbsp;<span class="inlinecode"><span class="id" title="var">nat</span></span>&nbsp;(because&nbsp;<span class="inlinecode">3</span>&nbsp;has<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;the&nbsp;type&nbsp;<span class="inlinecode"><span class="id" title="var">nat</span></span>).&nbsp;So,&nbsp;the&nbsp;variable&nbsp;<span class="inlinecode"><span class="id" title="var">m</span></span>&nbsp;gets&nbsp;instiated&nbsp;as&nbsp;<span class="inlinecode">3</span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="var">lets</span> <span class="id" title="var">K</span>: <span class="id" title="var">H</span> <a class="idref" href="LibTactics.html#::ltac_scope:'__'"><span class="id" title="notation">__</span></a> 3. <span class="comment">(*&nbsp;gives&nbsp;<span class="inlinecode"><span class="id" title="var">K</span></span>&nbsp;of&nbsp;type&nbsp;<span class="inlinecode">?<span class="id" title="var">X</span></span> <span class="inlinecode">≤</span> <span class="inlinecode">3</span> <span class="inlinecode">→</span> <span class="inlinecode">?<span class="id" title="var">X</span></span> <span class="inlinecode">&lt;</span> <span class="inlinecode">3+1</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">clear</span> <span class="id" title="var">K</span>.<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
Note: one can write <span class="inlinecode"><span class="id" title="var">lets</span>:</span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span> in place of <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode"><span class="id" title="var">H</span>:</span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span>.
    In this case, the name <span class="inlinecode"><span class="id" title="var">H</span></span> is chosen arbitrarily.

<div class="paragraph"> </div>

    Note: the tactics <span class="inlinecode"><span class="id" title="var">lets</span></span> accepts up to five arguments. Another
    syntax is available for providing more than five arguments.
    It consists in using a list introduced with the special symbol <span class="inlinecode">&raquo;</span>,
    for example <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode"><span class="id" title="var">H</span>:</span> <span class="inlinecode">(&raquo;</span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>3</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>4</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>5</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>6</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>7</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>8</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>9</sub></span></span> <span class="inlinecode">10)</span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="UseTactics.html#ExamplesLets"><span class="id" title="module">ExamplesLets</span></a>.<br/>
</div>

<div class="doc">
<a id="lab562"></a><h2 class="section">Working of <span class="inlinecode"><span class="id" title="var">applys</span></span>, <span class="inlinecode"><span class="id" title="var">forwards</span></span> and <span class="inlinecode"><span class="id" title="var">specializes</span></span></h2>

<div class="paragraph"> </div>

 The tactics <span class="inlinecode"><span class="id" title="var">applys</span></span>, <span class="inlinecode"><span class="id" title="var">forwards</span></span> and <span class="inlinecode"><span class="id" title="var">specializes</span></span> are
    shorthand that may be used in place of <span class="inlinecode"><span class="id" title="var">lets</span></span> to perform
    specific tasks.

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">forwards</span></span> is a shorthand for instantiating all the arguments

</li>
</ul>
    of a lemma. More precisely, <span class="inlinecode"><span class="id" title="var">forwards</span></span> <span class="inlinecode"><span class="id" title="var">H</span>:</span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>3</sub></span></span> is the
    same as <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode"><span class="id" title="var">H</span>:</span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>3</sub></span></span> <span class="inlinecode"><span class="id" title="var">___</span></span>, where the triple-underscore
    has the same meaning as explained earlier on.

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">applys</span></span> allows building a lemma using the advanced instantion

</li>
</ul>
    mode of <span class="inlinecode"><span class="id" title="var">lets</span></span>, and then apply that lemma right away. So,
    <span class="inlinecode"><span class="id" title="var">applys</span></span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>3</sub></span></span> is the same as <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode"><span class="id" title="var">H</span>:</span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>2</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>3</sub></span></span>
    followed with <span class="inlinecode"><span class="id" title="tactic">eapply</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> and then <span class="inlinecode"><span class="id" title="tactic">clear</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">specializes</span></span> is a shorthand for instantiating in-place

</li>
</ul>
    an assumption from the context with particular arguments.
    More precisely, <span class="inlinecode"><span class="id" title="var">specializes</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> is the same as
    <span class="inlinecode"><span class="id" title="var">lets</span></span> <span class="inlinecode"><span class="id" title="var">H'</span>:</span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="var">E<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">E<sub>1</sub></span></span> followed with <span class="inlinecode"><span class="id" title="tactic">clear</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> and <span class="inlinecode"><span class="id" title="tactic">rename</span></span> <span class="inlinecode"><span class="id" title="var">H'</span></span> <span class="inlinecode"><span class="id" title="var">into</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>.

<div class="paragraph"> </div>

    Examples of use of <span class="inlinecode"><span class="id" title="var">applys</span></span> appear further on. Several examples of
    use of <span class="inlinecode"><span class="id" title="var">forwards</span></span> can be found in the tutorial chapter <a href="UseAuto.html"><span class="inlineref">UseAuto</span></a>. 
</div>
<div class="code">
</div>

<div class="doc">
<a id="lab563"></a><h1 class="section">Summary</h1>

<div class="paragraph"> </div>

 In this chapter we have presented a number of tactics that help make
    proof script more concise and more robust on change.

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">introv</span></span> and <span class="inlinecode"><span class="id" title="var">inverts</span></span> improve naming and inversions.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">false</span></span> and <span class="inlinecode"><span class="id" title="var">tryfalse</span></span> help discarding absurd goals.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">unfolds</span></span> automatically calls <span class="inlinecode"><span class="id" title="tactic">unfold</span></span> on the head definition.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">gen</span></span> helps setting up goals for induction.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">cases</span></span> and <span class="inlinecode"><span class="id" title="var">cases_if</span></span> help with case analysis.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">splits</span></span> and <span class="inlinecode"><span class="id" title="var">branch</span></span>, to deal with n-ary constructs.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">asserts_rewrite</span></span>, <span class="inlinecode"><span class="id" title="var">cuts_rewrite</span></span>, <span class="inlinecode"><span class="id" title="var">substs</span></span> and <span class="inlinecode"><span class="id" title="var">fequals</span></span> help
      working with equalities.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">lets</span></span>, <span class="inlinecode"><span class="id" title="var">forwards</span></span>, <span class="inlinecode"><span class="id" title="var">specializes</span></span> and <span class="inlinecode"><span class="id" title="var">applys</span></span> provide means
      of very conveniently instantiating lemmas.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">applys_eq</span></span> can save the need to perform manual rewriting steps
      before being able to apply lemma.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">admits</span></span>, <span class="inlinecode"><span class="id" title="var">admit_rewrite</span></span> and <span class="inlinecode"><span class="id" title="var">admit_goal</span></span> give the flexibility to
      choose which subgoals to try and discharge first.

</li>
</ul>

<div class="paragraph"> </div>

    Making use of these tactics can boost one's productivity in Coq proofs.

<div class="paragraph"> </div>

    If you are interested in using <span class="inlinecode"><span class="id" title="var">LibTactics.v</span></span> in your own developments,
    make sure you get the lastest version from:
    <a href="https://www.chargueraud.org/softs/tlc/"><span class="inlineref">https://www.chargueraud.org/softs/tlc/</span></a>.

<div class="paragraph"> </div>


</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;2020-08-24&nbsp;16:13&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>